es:ES, i:Id, P:({e:E| loc(e) = i }{e2:E| loc(e2) = i }Prop).
e1@i. e2e1.(e:E. (e1 <loc e)  e  e2   P(e,e2))  P(e1,e2)
 e1@i. e2<e1. P(e1,e2)
 (e, e':E. loc(e) = i  loc(e') = i  P(e,e')) 

latex

Definitions	t  T, P  Q, x:A. B(x), loc(e), Id, E, b, False, A, Prop, x(s1,s2), x. t(x), e<e'. P(e), e@i. P(e), P & Q, (e <loc e'), ES, 1of(t), P  Q, e  e' , e'e.P(e'), Dec(P), P  Q
Lemmas	not functionality wrt iff, es-le-not-locl, not wf, decidable es-locl, decidable es-le, event system wf, alle-ge wf, es-locl wf, es-le wf, es-le-loc, alle-at wf, alle-lt wf, subtype rel self, es-loc-pred, es-E wf, Id wf, es-loc wf, es-interval-induction